\begin{tabbing}
$\forall$\=$i$:Id, ${\it ds}$:fpf(Id; $x$.Type), ${\it da}$:fpf(Knd; $k$.Type), $x$:Id, $T$:Type, ${\it ks}$:(Knd List),\+
\\[0ex]${\it tr}$:($k$:\{$k$:Knd$\mid$ ($k$ $\in$ ${\it ks}$)\} $\rightarrow$decl{-}state(${\it ds}$)$\rightarrow$ma{-}valtype(${\it da}$; $k$)$\rightarrow$$T$$\rightarrow$$T$).
\-\\[0ex]fpf{-}compatible(Id; $x$.Type; id{-}deq; ${\it ds}$; fpf{-}single($x$; $T$))
\\[0ex]$\Rightarrow$ (R{-}state{-}var($i$; ${\it ds}$; ${\it da}$; $x$; $T$; ${\it ks}$; ${\it tr}$) $\in$ es\_realizer\{i:l\})
\end{tabbing}